A, B, C:Realizer. R-Feasible(C)  A  C  B  C  A || B 

latex

Definitions

x:A. B(x), P  Q, t  T, AB, A, False, ij, A || B, Rplus?(x1), P & Q, Rplus-left(x1), Rplus-right(x1), Y, if b t else f fi, Rnone?(x1), true, false, Prop, SQType(T), {T}, , , Dec(P), P  Q, A  B, , Unit, P  Q, R-Feasible(R),

Lemmas

nat wf, R-size wf, nat plus wf, R-sub wf, R-Feasible wf, es realizer wf, le wf, nat properties, ge wf, decidable assert, Rplus? wf, R-size-decreases, Rplus-implies, Rplus-left wf, Rplus-right wf, Rnone? wf, Rnone-implies, R-compat-none, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, R-compat-symmetry, Rnone wf, R-compat wf, bool cases, bool sq, R-sub-self, R-compat-self